
{-

Reworked parser

-}

module SParser where


import Control.Monad.Error
import Data.Maybe
import Data.Either
import Numeric
import Data.Set as Set (fromList,empty)

-- import Debug.Trace.Location
import Maybe
import RPTypes

import Data.Map (Map,empty,lookup,insert,fromList)
import IO

-- types for error handling

import Debug.Trace
mtrace x = (trace ("MTRACE: " ++ (show x)) x)

type ParseMonad = Either ParseError

instance Error ParseError where

{-
instance MonadError (Either ParseError) where 
    throwError = Left 
    (Left e) `catchError` handler = handler e 
    a        `catchError` _       = a 
-}

data ParseError = 
	PointError String Position
       |RangeError String Position Position               

instance Show ParseError where 
    show (PointError s (POS l c f)) 
       = "in file " ++ f ++ ", line " ++ (show l) ++ ", char " ++ (show c) ++ "; " ++ s

lexError s p = throwError $ PointError s p
parseError s (TKN p tok) = throwError $ PointError ("found " ++ (show tok)++ " " ++s) p 

-- currently for equal priority everything is bracketed (a op (b op c))
-- this screws up arithmetic a bit but can be fixed by bracketing the program

maxPrio = 1200

som =      [(":-", (1150,XFX)), -- should also be FX, hack in isUnaryOperator to deal with this
            (":::", (1100, XFX)), -- matrix <-> quantifier connective
            ("=>", (1075, XFY)), -- implication, turned into rnot A or B
            (",", (1050, XFY)),
            ("~", (1050, XFX)), -- quantifier symbol <-> quantifier variable connective
            (";", (1000,XFY)), --- I personally believe this should be higher but this seems standard
            ("rnot", (900,FX)),
            ("is", (800,XFX)),
            ("\\=", (700, XFX)),
            ("\\==", (700, XFX)),
            ("=", (700, XFX)),
	    ("<", (700,XFX)),
	    (">", (700,XFX)),
	    (">=", (700,XFX)),
	    ("=<", (700,XFX)),
	    ("=:=", (700,XFX)),
	    ("@<", (700,XFX)),
	    ("@>", (700,XFX)),
	    ("@>=", (700,XFX)),
	    ("@=<", (700,XFX)),
	    ("=@=", (700,XFX)),	    
            ("+", (500,XFY)),
	    ("-", (500,XFY)),
            ("*", (400,XFY)),
	    ("/", (400,XFY))]

startOpMap :: OpMap
startOpMap = Data.Map.fromList som

-- parseResult a = Right 

--
-- Interface code; ties analyser and parser together
--

-- readTerm - interface for builtin
readInputTerm :: IO (ParseMonad Term)
readInputTerm   = 
             do putStr ("Enter Term: ")
                line1 <- getLine
                putStrLn ("Result is:\n" ++ line1 ++ "\n")
                return (parseString line1 1)
             where parseString x n = parseTerm $ markString ("Interactive interpreter " ++ show n) x


-- this is only used internally, and we write perfect prolog! (mostly)
stringToCBody :: String -> [CBody]
stringToCBody str = 
    (fromRight ((pasres $ markString "" (str ++ ".")) `catchError` printError))
    where
        pasres s = do l <- lexAnalyse s []
                      r <- (toksToTerms l [] startOpMap)
                      ll <- (mapM clauseBody (deListify r))
                      return ll
        -- printError _ = Right undefined
        printError e = trace ("Internal Error: " ++ (show e)) (Right undefined)


-- this is only used internally, and we write perfect prolog!
stringToTerm :: String -> Term
stringToTerm str = 
    (fromRight ((parseTerm $ markString "" str) `catchError` printError))
    where
        -- printError _ = Right undefined
        printError e =  (Right undefined)

fileToClauses :: String -> IO [Clause]
fileToClauses filename =
    do h <- openFile filename ReadMode
       str <- hGetContents h
       either (printError) (return) (parseClauses $ markString filename str)
	   where 
	       printError e = do putStrLn ("PARSE ERROR: " ++ (show e))
	                         return []

fromRight :: Either a b -> b	
fromRight (Right x) = x

markString :: String -> String -> PosString
markString filename s = 
   m1 s 1 1
   where
     m1 ('\n':r) char line = ((POSCHAR '\n' (makePos line char filename)) :
                                      (m1 r 1 (line + 1)))
     m1 (c:r) char line = ((POSCHAR c (makePos line char filename)):
                                      (m1 r (char + 1) line))
     m1 [] _ _ = []

parseClauses :: PosString -> ParseMonad [Clause]
parseClauses s = do l <- lexAnalyse s []
                    r <- (toksToTerms l [] startOpMap)
                    ll <- (termsToClauses$ deListify r)
                    return ll
{-
parseClauses :: PosString -> ParseMonad [Term]
parseClauses s = do l <- lexAnalyse s []
                    (toksToTerms l [] startOpMap)
-}

parseTerm :: PosString -> ParseMonad Term
parseTerm s = do l <- lexAnalyse s []
                 (toks,term) <- readTerm l startOpMap
                 if length toks /= 1 -- TOKEOF
                    then parseError "Extra stuff at end of term" (car toks)
                    else return term
              where
                 car (x:_) = x
--

dLL :: Term -> Term
dLL (T a n l p) = (T a n (deListify l) p)
dLL (L l p) = dll1 l p
dLL x = x

deListify :: [Term] -> [Term]
deListify x = map dLL x

dll1 (LE a b) p = (T "." 2 [(dLL a),(dll1 b p)] p)
dll1 (LNil) p = (T "[]" 0 [] p)
dll1 (LTerm x) p = dLL x

termsToClauses :: [Term] -> ParseMonad [Clause]
termsToClauses t = mapM termToClause t

termToClause (T ":-" 2 [h,b] p) = do cb <- clauseBody b 
                                     return (CLA h cb)
termToClause (T ":-" 1 [b] p) = return (DIR b)
termToClause x = return (CLA x CNIL)

-- dies both clauses and queries; not sure what happens when we have query stuff in clauses ...
clauseBody :: Term -> ParseMonad CBody
clauseBody (T "," 2 [a,b] pos) = do ca <- clauseBody a
                                    cb <- clauseBody b
                                    return (CCONJ ca cb Notset)
clauseBody (T ";" 2 [a,b] pos) =  do ca <- clauseBody a
                                     cb <- clauseBody b
                                     return (CDISJ ca cb Notset)
--clauseBody [] =
--- clauseBody (T "-" 2 [(T "exists" 0 []),(V x)]) = CQUANT Exists [(V x)] 
clauseBody (T ":::" 2 [l,r] pos) = queryParts (T ":::" 2 [l,r] pos)
clauseBody (T "rnot" 1 [a] pos) = do ab <- clauseBody a
                                     return (CNOT ab Notset)
clauseBody x = return (CTERM x Notset)

queryParts :: Term -> ParseMonad (CBody) 
queryParts (T ":::" 2 [l,r] pos) = 
    do (q,v) <- parseQuant l 
       b <- clauseBody r
       if q == Exists
         then return (CQUANT [Set.fromList v] b Notset)
         else return (CQUANT [Set.empty,Set.fromList v] b Notset)
queryParts t = queryError "Error in query; should be of form 'E ::: M'; E existential spec, M matrix" (getTPos t)

parseQuant :: Term -> ParseMonad (Quantifier,[Term])
parseQuant (T "," 2 [l,r] pos) =
    do (q0,r) <- parseQuant r
       (q1,h) <- parseQ l
       if q0 == q1 
         then return (q0,(h:r))
         else queryError ("Quantifier type " ++ (show q0) ++ " not equal to " ++ (show q1)) pos
parseQuant t =
    do (q,h) <- parseQ t 
       return (q,[h])

parseQ :: Term -> ParseMonad (Quantifier,Term)
parseQ (T "~" 2 [(T quant 0 [] pos),(V x p)] _) = 
    do q <- parseQSymb quant pos
       return (q,(V x p))
parseQ t = queryError ("Error in quantifier specification, should be of form '[exists|forall] ~ X' " ++ (show t)) (getTPos t)

parseQSymb :: String -> Position -> ParseMonad Quantifier
parseQSymb "exists" _ = return Exists
parseQSymb "forall" _ = return Forall
parseQSymb x pos = queryError ("Unrecognized quantifier symbol " ++ x) pos

toksToTerms:: [Token] -> [Term] -> OpMap -> ParseMonad [Term]
toksToTerms [] cl _ = return (reverse cl)
toksToTerms (t:ts) cl opmap =
                   if (isTokenEOF t)
                      then return (reverse cl)
                      else do (tokenrest,term) <- readTermSequence (t:ts) NullTerm opmap TokPeriod
                              toksToTerms tokenrest (term:cl) opmap
                              -- ((toksToTerms $! tokenrest) $! (mtrace (term:cl))) opmap

readPeriod :: [Token] -> ParseMonad [Token] 
readPeriod (t:ts) = 
                if (getTokSymb t) /= TokPeriod
                    then parseError "Expected Period" t
                    else return ts

-- Call: (toks,term) = readTermSequence toks0 term0 opmap

data Precedence = FX | XFY | YFX | XFX
                deriving Eq

type OpMap = Map Atom (Integer,Precedence)
getPriority :: Atom -> OpMap -> Maybe Integer
getPriority a m = maybe Nothing (Just . fst) (Data.Map.lookup a m )

isOp a m = let res = isJust (Data.Map.lookup a m)
           -- in trace ("looking up " ++ a ++ " got " ++ (show $! res)) res
           in res

-- big ugly hack for unary neck ...
isUnaryOperator :: TokSymb -> OpMap -> Bool
isUnaryOperator TokNeck _ = True
isUnaryOperator (TokStr s) map = maybe False (\x -> (snd x == FX)) (Data.Map.lookup s map)
isUnaryOperator _ _ = False

readTermSequence :: [Token] -> Term -> OpMap -> TokSymb -> ParseMonad ([Token],Term)
-- [Token] == [] is an internal error
readTermSequence [tok] _ _ _ = parseError "Unexpected token" tok
readTermSequence (t1:resttok) currterm opmap endtok =
    case (getTokSymb t1) of
    ts | ts == endtok -> return (resttok,currterm)
       -- essentially assumes unary ops occur only when currterm == NullTerm XXX - needs to be extended for general unary ops.
       | (isUnaryOperator ts opmap) -> 
           do (tok0,newterm) <- readTermSequence resttok NullTerm opmap endtok
              return (tok0,insertFinTerm currterm (T (getAtom t1) 1 [newterm] (getTokPos t1)))
       | otherwise -> do (tok0,newterm) <- readTerm (t1:resttok) opmap
                         (tok1,op) <- readOperator tok0 opmap
                         if isNothing op
                            then return (tok1,insertFinTerm currterm newterm)
                            else readTermSequence tok1
                                                  (insertSeqTerm currterm newterm (getAtom $ fromJust $ op) opmap)
                                                  opmap
                                                  endtok
                                             

{- 
This next bit is ugly and must go -> we should lex into atoms and symbol-ops only, 
and then get the role post the token-parse.
-}
getAtom (TKN _ TokNeck) = ":-"
getAtom (TKN _ TokComma) = ","
getAtom (TKN _ TokSemiColon) = ";"
getAtom x = string $ getTokSymb x                      

readOperator:: [Token] -> OpMap -> ParseMonad ([Token],Maybe Token)
readOperator (start:rest) opmap = 
     case (getTokSymb start) of
     TokPeriod -> return (rest,Nothing)
     TokCloseBrak -> return (rest,Nothing)
     TokOpenBrak -> return (rest,Nothing)
     TokNeck -> return (rest,Just start)
     TokEOF -> return (rest,Nothing)
     otherwise -> do if isOp (getAtom start) opmap 
                        then return (rest,Just start)
                        else parseError ("Expected operator or terminator, got " ++ (getAtom start)) start

readOperator [] _ = parseError "Expected operator or terminator" tokenEOF

-- insertTermSequence oldterm newterm opmap
insertFinTerm (NullTerm) t = t
insertFinTerm (T atom 2 [t1,t2] pos) tf = (T atom 2 [t1,insertFinTerm t2 tf] pos)

insertSeqTerm :: Term -> Term -> Atom -> OpMap -> Term
insertSeqTerm (T cat 2 [ct1,ct2] pos) tf op opmap = 
     let newprio = getPriority op opmap
         oldprio = getPriority cat opmap
     in if (newprio > oldprio)
        then (T op 2 [insertFinTerm (T cat 2 [ct1,ct2] pos) tf,NullTerm] (getTPos tf))
        else (T cat 2 [ct1,insertSeqTerm ct2 tf op opmap] pos)
insertSeqTerm NullTerm t op _ = (T op 2 [t,NullTerm] (getTPos t)) 

-- parses comma separated list of list members
readTermListSQB :: [Token] -> OpMap -> ParseMonad ([Token],ListTerm)
readTermListSQB (t:ts) opmap = 
    case (getTokSymb t) of
    TokCloseSqBrak -> return (ts,LNil)
    otherwise ->
	do (nt0,t1) <- readTerm (t:ts) opmap
	   (nt,ts) <- readTermListPE nt0 opmap
	   return (nt,(LE t1 ts))

readTermListPE :: [Token] -> OpMap -> ParseMonad ([Token],ListTerm)
readTermListPE (t:ts) opmap = 
    case (getTokSymb t) of
    TokCloseSqBrak -> return (ts,LNil)
    TokComma ->
	do (nt0,t1) <- readTerm ts opmap
	   (nt,ts) <- readTermListPE nt0 opmap
	   return (nt,(LE t1 ts))
    TokListRest ->
	do ((nt:nts),t1) <- readTerm ts opmap
	   if (getTokSymb nt) == TokCloseSqBrak
	      then return (nts,(LTerm t1))
	      else parseError "Expected ']'" nt
    otherwise -> parseError "Unexpected Token" t

-- parses comma separeted list of predicate/function arguments
readTermList :: [Token] -> OpMap -> ParseMonad ([Token],[Term])
readTermList ts opmap
             = do ((nt:nts0),t1) <- readTerm ts opmap
                  if (getTokSymb nt) == TokComma
                        then do (nts1,tr) <- readTermList nts0 opmap
                                return (nts1,t1:tr)
                        else return ((nt:nts0),[t1])

--- XXX fails for unary operators at the beginning of a term followed by a bracket.
readTerm :: [Token] -> OpMap -> ParseMonad ([Token],Term)
readTerm (t:ts) opmap =
     let toksymb = getTokSymb t
         pos = getTokPos t
	 s = (getTokStr toksymb)
	 v = (getTokVar toksymb)
	 i = (getTokInt toksymb)
	 f = (getTokFloat toksymb)
	 variable = (V v pos)
	 atom = (T s 0 [] pos)
	 intterm = (I i pos)
	 floatterm = (F f pos)
	 (x:xs0) = ts
	 in case toksymb of
		(TokVar _) -> return (ts,variable)
		(TokCut) -> return (ts,CutTerm pos)
		(TokOpenSqBrak) ->
		    do (xss,tlist) <- readTermListSQB ts opmap
		       return (xss,(L tlist pos))
		(TokOpenBrak) -> 
	            do (as,b) <- readTermSequence ts (NullTerm) opmap TokCloseBrak
		       return (as,b)
		(TokStr _) -> 
		    case (getTokSymb x) of -- x == next token
			 tx | tx == TokOpenBrak -> 
				do ((x1:xs1),tlist) <- readTermList xs0 opmap
				   if getTokSymb x1 /= TokCloseBrak
				      then parseError "Expected Close Bracket" x1
                                      else return (xs1,(T s (fromIntegral (length tlist)) tlist pos))
			    | tx == TokComma -> return ((x:xs0),atom)
                            | tx == TokNeck -> return ((x:xs0),atom)
                            | tx == TokSemiColon -> return ((x:xs0),atom)
                            | tx == TokPeriod -> return ((x:xs0),atom)
                            | tx == TokCloseBrak -> return ((x:xs0),atom)
			    | tx == TokCloseSqBrak -> return ((x:xs0),atom)
			    | tx == TokListRest -> return ((x:xs0),atom)
			    | (isInt tx) -> return ((x:xs0),intterm)
			    | (isFloat tx) -> return ((x:xs0),floatterm)
                            | (isStr tx) && isOp (string tx) opmap -> return ((x:xs0),atom)
                            | otherwise -> parseError "Expected Open Bracket or Term Delimiter" x
		otherwise -> parseError "Expected Atom or Variable" t

isStr (TokStr _) = True
isStr (TokUnknown _) = True
isStr _ = False

isInt (TokInt _) = True
isInt _ = False

isFloat (TokFloat _) = True
isFloat _ = False

-- readPredicate :: (MonadState ParseData (ParserAction m h)) => ParserAction m h Term
readPredicate = readTerm

--
-- Lexical analyser
--  Note these can throw EOFs (and presumably other) exceptions - this has 
--  to be dealt with one level up 
--

whitespace = [' ','\t','\n','\r'] -- I think windows maps \r\n -> \n internally ...
namechars = ['a'..'z']++['A'..'Z']++['_']++['0'..'9'] ++ ['$']
varchars = ['A'..'Z']++['_']
numchars = ['0'..'9']
numcharsall = ['0'..'9'] ++ ['.']
atomchars = ['a'..'z'] ++ numchars ++ ['$']
brakchar = ['(',')','{','}','[',']']
miscchar = [':' , '-' , ';' ,'/', '*' , '+' , '=','\\','|','>','<','@','~'] 
nongroupmiscchar = ['.','!']

dropPercentComment :: PosString -> PosString
dropPercentComment (ps:pss) = 
                          if (ch ps == '\n')
                             then pss
                             else dropPercentComment pss
dropPercentComment [] = []

dropSlashComment :: PosString -> PosString
dropSlashComment (ps:pss) =
                        if (ch ps == '*')
                           then drest pss
                           else dropSlashComment pss
                        where
                           drest (ps:pss) =
                                   if (ch ps == '/')
                                      then pss
                                      else dropSlashComment (ps:pss)
dropSlashComment [] = []

lexset :: [Char] -> String -> PosString -> (PosString,String,Position)
lexset charset s (ps:pss) = 
                        if ((ch ps) `elem` charset)
                          then lexset charset (s++[ch ps]) pss
                          else ((ps:pss),s,pos ps)
lexset _ s [] = ([],s,nullpos)

-- Either -- Left == error,
--           Right == Ok

lexAnalyse :: PosString -> [Token] -> ParseMonad [Token]
lexAnalyse [] tok = let res = (reverse (tokenEOF:tok))
                    in return res
lexAnalyse (ps:pss) tok = 
             let start = pos ps
             in (case ch ps of
	           c | c `elem` whitespace -> lexAnalyse pss tok
	             | c == '`' -> lexAnalyse ((markString "NOFILE" "$evidence") ++ pss) tok
	             | c == '%' -> lexAnalyse (dropPercentComment pss) tok
	             | c == '/' -> let (nps:npss) = pss
	                           in if ch nps /= '*'
	                                 then let (rest,tokstr,end) = lexset miscchar [c] pss
	                                          in lexAnalyse rest ((miscTok tokstr start end):tok)
	                                 else lexAnalyse (dropSlashComment pss) tok
	             | c == ',' -> lexAnalyse pss ((miscTok [c] start start):tok)
		     | c `elem` numchars  -> 
	                          let (rest,tokstr,end) = lexset numcharsall [c] pss
	                          in lexAnalyse rest ((stringTok tokstr start end):tok)
	             | c `elem` atomchars  -> 
	                           let (rest,tokstr,end) = lexset namechars [c] pss
	                           in lexAnalyse rest ((stringTok tokstr start end):tok)
	             | c `elem` varchars  -> 
	                           let (rest,tokstr,end) = lexset namechars [c] pss
	                           in lexAnalyse rest ((varTok tokstr start end):tok)
	             | c `elem` brakchar -> -- note "))" should be two tokens ...
	                           lexAnalyse pss ((bracketTok [c] start start):tok)
	             | c `elem` nongroupmiscchar ->
	                           lexAnalyse pss ((miscTok [c] start start):tok)	             
	             | c `elem` miscchar -> 
	             	           let (rest,tokstr,end) = lexset miscchar [c] pss
	                           in lexAnalyse rest ((miscTok tokstr start end):tok)	             
	             | otherwise -> lexError ("Unknown symbol "++[c]) start )

stringTok :: String -> Position -> Position -> Token
stringTok s p _ = (TKN p (TokStr s))

intTok :: String -> Position -> Position -> Token
intTok s p _ = (TKN p (TokInt i))
	       where [(i,"")] = (readSigned readDec s)

varTok :: String -> Position -> Position -> Token
varTok s p _ = (TKN p (TokVar s))

bracketTok :: String -> Position -> Position -> Token
bracketTok s p _
	| s == "(" = (TKN p TokOpenBrak)
	| s == ")" = (TKN p TokCloseBrak)
        | s == "[" = (TKN p TokOpenSqBrak)
        | s == "]" = (TKN p TokCloseSqBrak )
	| otherwise = (TKN p (TokUnknown s))
	
miscTok :: String -> Position -> Position -> Token
miscTok s p _
	| s == ":-" = (TKN p TokNeck)
	| s == ";" = (TKN p TokSemiColon)
	| s == "," = (TKN p TokComma)
	| s == "." = (TKN p TokPeriod)
	| s == "!" = (TKN p TokCut)
	| s == "|" = (TKN p TokListRest)
	| otherwise = (TKN p (TokUnknown s))

queryError x y = Left (PointError x y)





--
-- Misc
--

instance Ord Clause where
    compare (CLA t1 _) (CLA t2 _) = compare t1 t2
    


tokenEOF::Token
tokenEOF = TKN (POS 0 0 "") TokEOF


isTokStr:: TokSymb -> Bool
isTokStr (TokStr _) = True
isTokStr _ = False

getTokStr:: TokSymb -> String
getTokStr (TokStr s) = s

getTokVar (TokVar s) = s

getTokInt (TokInt i) = i

getTokFloat (TokFloat f) = f

getTokSymb:: Token -> TokSymb
getTokSymb (TKN _ t) = t

getPos:: Token -> Position
getPos (TKN p _) = p

isTokenEOF t = (getTokSymb t) == TokEOF

